FDL - Nuprl Lemma : can-apply-fun-exp-add

Nuprl Lemma : can-apply-fun-exp-add

A:Type, n, m:

, f:(A

(A + Top)), x:A.
(

can-apply(f^n+m;x))

{(

can-apply(f^m;x))

& (

can-apply(f^n;do-apply(f^m;x)))

& do-apply(f^n+m;x) = do-apply(f^n;do-apply(f^m;x))

A}

Definitions P Q, x:A. B(x), f^n, x:AB(x), P Q, t T, True, T, b, Top, left + right, Type, do-apply(f;x), s = t, x:A B(x), P & Q, P Q, False, A, A B, , {x:A| B(x)} , , {T}, S T, suptype(S; T), can-apply(f;x), ,

Lemmas assert wf, can-apply wf, can-apply-compose, do-apply wf, p-fun-exp-add, do-apply-compose